1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
use super::*;
#[derive(Debug, Clone, Eq, PartialEq, Hash)]
pub struct ReduceUntil<R, C> {
pub reduce: R,
pub until: C,
}
impl<R, C> ReductionConfig for ReduceUntil<R, C>
where
R: ReductionConfig,
C: TerminationCondition,
{
type AsRef = Self;
#[inline]
fn register_push_subst(&mut self, subst: &TermId) -> Result<(), Error> {
self.reduce.register_push_subst(subst)
}
#[inline]
fn register_pop_subst(&mut self) -> Result<(), Error> {
self.reduce.register_pop_subst()
}
#[inline]
fn register_beta(&mut self) -> Result<(), Error> {
self.reduce.register_beta()
}
#[inline]
fn register_eta(&mut self) -> Result<(), Error> {
self.reduce.register_eta()
}
#[inline]
fn eta(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
if self.until.terminate(term, ctx) {
return Err(Error::StopReduction);
}
self.reduce.eta(term, ctx)
}
#[inline]
fn sub(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
if self.until.terminate(term, ctx) {
return Err(Error::StopReduction);
}
self.reduce.sub(term, ctx)
}
#[inline]
fn head(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> Result<bool, Error> {
if self.until.terminate(term, ctx) {
return Err(Error::StopReduction);
}
self.reduce.head(term, ctx)
}
#[inline]
fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool {
self.reduce.intersects(filter, code, form)
}
#[inline]
fn as_ref_mut(&mut self) -> &mut Self::AsRef {
self
}
}
pub trait TerminationCondition {
fn terminate(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> bool;
}
impl TerminationCondition for TermId {
#[inline]
fn terminate(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> bool {
let result = self.eq_term_in(term, ctx.eq_ctx());
result.is_some()
}
}
impl TerminationCondition for Option<TermId> {
#[inline]
fn terminate(&self, term: &Term, ctx: &mut (impl TyCtxMut + ?Sized)) -> bool {
if let Some(this) = self {
this.terminate(term, ctx)
} else {
false
}
}
}